Covered languages in this unit will all be computable/decidable which means we will be working in intuitionistic logic.

Terminology

A judgement is a claim that something holds some property. In order to prove it is true, we must provide some evidence using rules, once that is done, it is an evidenced judgement.

Rules have names, and consist of some (possibly none) premises which are placed on the top, and a conclusion which goes on the bottom. The name goes to the right of these. A rule with no premises, is an axiom.

---

Our Rules

Proofs

Proof that two is a natural number

Proof that two is even

Derivable & Admissible Rules

An admissible rule is any rule that is not necessary, i.e. a rule where if we have a derivation of the premise, we know that we can construct a derivation of the conclusion.

A rule is derivable if we can use a derivation of its premise (what goes on top) as a building block in deriving its conclusion.

Example of a Derivable Rule

Not every admissible rule is derivable, but if a rule is derivable it is admissible.

This rule is admissible but not derivable, because anything we could assemble with it, we could do with the existing $S$ rule:

Induction

Cards

Q: What is the relationship between derivable and admissible rules? A: Derivable => admissible, but not the reverse

Q: What is the structure of a rule? A: